(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun mem_35_149 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EBX_6_86 () (_ BitVec 32))
(declare-fun R_ESI_2_79 () (_ BitVec 32))
(declare-fun R_EBP_0_73 () (_ BitVec 32))
(declare-fun R_ESP_1_69 () (_ BitVec 32))
(assert (let ((?v_1 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_149 (bvadd (_ bv134560456 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_149 (bvadd (_ bv134560456 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_149 (bvadd (_ bv134560456 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_149 (bvadd (_ bv134560456 32) (_ bv3 32)))) (_ bv24 32)))) (?v_3 (bvsub R_ESP_1_69 (_ bv4 32)))) (let ((?v_6 (store (store (store (store mem_35_149 (bvadd ?v_3 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_73 (_ bv24 32)))) (bvadd ?v_3 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_73 (_ bv16 32)))) (bvadd ?v_3 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_73 (_ bv8 32)))) (bvadd ?v_3 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_73)))) (let ((?v_15 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_6 (bvadd (_ bv134560596 32) (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_6 (bvadd (_ bv134560596 32) (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_6 (bvadd (_ bv134560596 32) (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_6 (bvadd (_ bv134560596 32) (_ bv3 32)))) (_ bv24 32)))) (?v_4 (bvsub ?v_3 (_ bv4 32))) (?v_0 (bvnot (_ bv0 1)))) (let ((?v_5 (bvsub ?v_4 (_ bv4 32)))) (let ((?v_7 (store (store (store (store (store (store (store (store ?v_6 (bvadd ?v_4 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_ESI_2_79 (_ bv24 32)))) (bvadd ?v_4 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_ESI_2_79 (_ bv16 32)))) (bvadd ?v_4 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_ESI_2_79 (_ bv8 32)))) (bvadd ?v_4 (_ bv0 32)) ((_ extract 7 0) R_ESI_2_79)) (bvadd ?v_5 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_86 (_ bv24 32)))) (bvadd ?v_5 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_86 (_ bv16 32)))) (bvadd ?v_5 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_86 (_ bv8 32)))) (bvadd ?v_5 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_86))) (?v_2 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (bvor (bvxor (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr ?v_1 (_ bv31 32)))) (_ bv1 1) (_ bv0 1)) (_ bv0 1)) (ite (= ?v_1 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (?v_8 (bvadd ?v_15 (_ bv8 32)))) (let ((?v_9 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_7 (bvadd ?v_8 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_8 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_8 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_8 (_ bv3 32)))) (_ bv24 32))))) (let ((?v_10 (bvsub ?v_9 (_ bv1 32)))) (let ((?v_17 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (bvor (ite (bvult ?v_9 (_ bv1 32)) (_ bv1 1) (_ bv0 1)) (ite (= ?v_10 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (?v_12 (bvadd (_ bv0 32) (_ bv1 32))) (?v_16 (bvneg (_ bv1 32)))) (let ((?v_11 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor (_ bv0 32) (bvxor (_ bv1 32) ?v_16)) (bvxor (_ bv0 32) ?v_12)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_13 (bvsub ?v_12 ?v_1))) (let ((?v_14 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_13 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (let ((?v_18 (bvand ?v_11 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_12 ?v_1) (bvxor ?v_12 ?v_13)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_14 (_ bv1 1)) (bvor (bvnot ?v_14) (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_15 (bvxor (_ bv40 32) ?v_16)) (bvxor ?v_15 (bvadd ?v_15 (_ bv40 32)))) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (_ bv0 1)))))))) (let ((?v_30 (bvand ?v_11 ?v_18)) (?v_19 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (concat (_ bv0 24) (select ?v_7 (_ bv134560400 32))))) (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (?v_20 (bvadd ?v_15 (_ bv24 32)))) (let ((?v_21 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_7 (bvadd ?v_20 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_20 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_20 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_20 (_ bv3 32)))) (_ bv24 32))))) (let ((?v_22 (bvsub ?v_21 (_ bv0 32)))) (let ((?v_23 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_21 (_ bv0 32)) (bvxor ?v_21 ?v_22)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (let ((?v_24 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (bvor (bvxor (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr ?v_22 (_ bv31 32)))) (_ bv1 1) (_ bv0 1)) ?v_23) (ite (= ?v_22 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))) (?v_25 (bvadd ?v_15 (_ bv28 32)))) (let ((?v_26 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_7 (bvadd ?v_25 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_25 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_25 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_7 (bvadd ?v_25 (_ bv3 32)))) (_ bv24 32))))) (let ((?v_27 (bvsub ?v_26 (_ bv0 32)))) (let ((?v_28 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_26 (_ bv0 32)) (bvxor ?v_26 ?v_27)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (let ((?v_29 (bvnot ((_ extract 0 0) (concat (_ bv0 31) (bvor (bvxor (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr ?v_27 (_ bv31 32)))) (_ bv1 1) (_ bv0 1)) ?v_28) (ite (= ?v_27 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (= (_ bv1 1) (bvand ?v_0 (bvand ?v_0 (bvand (bvor ?v_2 (_ bv1 1)) (bvor (bvnot ?v_2) (bvand ?v_0 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_9 (_ bv1 32)) (bvxor ?v_9 ?v_10)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand (bvor ?v_17 ?v_30) (bvor (bvnot ?v_17) (bvand ?v_0 (bvand (bvor ?v_19 ?v_18) (bvor (bvnot ?v_19) (bvand (bvnot ?v_23) (bvand (bvor ?v_24 ?v_18) (bvor (bvnot ?v_24) (bvand (bvnot ?v_28) (bvand (bvor ?v_29 ?v_18) (bvor (bvnot ?v_29) ?v_30)))))))))))))))))))))))))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
